\begin{tabbing}
frame{-}p(${\it es}$; $i$; $T$; $x$; $L$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); $T$)\+
\\[0ex]c$\wedge$ alle{-}at(\=${\it es}$;\+
\\[0ex]$i$;
\\[0ex]$e$.(($\neg$(es{-}kind(${\it es}$; $e$) $\in$ $L$ $\in$ Knd))
\\[0ex]$\Rightarrow$ \=($\forall$$t$:rationals. \+
\\[0ex]es\_state\_after(${\it es}$; $e$)($x$,$t$) = es\_state\_when(${\it es}$; $e$)($x$,$t$) $\in$ $T$)))
\-\-\-
\end{tabbing}